(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.

(** Sk -> Sb *)

(* 侧滑角β (sidelip angle) *)
Parameter beta : R.

(* 迎角 α  (angle of attack) *)
Parameter alpha : R.

(* γ  *)
Parameter gamma : R.

Definition coordinate_transform_SaSb : Mat R 3 3 := mkMat_3_3
  ((cos alpha)*(cos beta)) (-(cos alpha)*(sin beta)) (-sin alpha)
  (sin beta)                (cos beta)                    0
  ((sin alpha)*(cos beta)) (-(sin alpha)*(sin beta)) (cos alpha).

Definition coordinate_transform_SkSa : Mat R 3 3 := mkMat_3_3
  1      0            0
  0 (cos gamma) (-sin gamma)
  0 (sin gamma) (cos gamma).

Definition SkToSb :Mat R 3 3 := mkMat_3_3
  ((cos alpha)*(cos beta))
  (-(cos gamma)*(cos alpha)*(sin beta)-(sin gamma)*(sin alpha))
  ((sin gamma)*(cos alpha)*(sin beta)-(cos gamma)*(sin alpha))
  (sin beta) ((cos gamma)*(cos beta)) (-(sin gamma)*(cos beta))
  ((sin alpha)*(cos beta)) 
  (-(cos gamma)*(sin alpha)*(sin beta)+(sin gamma)*(cos alpha))
  ((sin gamma)*(sin alpha)*(sin beta)+(cos gamma)*(cos alpha)).

Lemma SkToSb_eq:
  SkToSb === RMmul coordinate_transform_SaSb coordinate_transform_SkSa.
Proof. unfold SkToSb.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal3. ring. f_equal. ring. f_equal. ring. f_equal. ring.
  f_equal2. ring. f_equal. ring.
Qed.


